Nuprl Lemma : assert_of_dset_eq
13,42
postcript
pdf
s
:DSet,
a
,
b
:|
s
|. (
(
a
(=
)
b
))
(
a
=
b
)
latex
Up
sets
1
Definitions of Statement
DSet
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
DSet
,
IsEqFun(
T
;
eq
)
Lemmas
dset
wf
,
set
car
wf
,
dset
properties
origin
s:DSet, a, b:|s|. (
(a (=
) b)) 
(a = b) s:DSet, a, b:|s|. ((a (=) b)) (a = b) 
Tx:A. B(x)